Nuprl Lemma : no_repeats_nil
11,40
postcript
pdf
T
:Type. no_repeats(
T
; [])
latex
Definitions
prop{i:l}
,
t
T
,
False
,
Y
,
A
,
||
as
||
,
P
Q
,
no_repeats(
T
;
l
)
,
x
:
A
.
B
(
x
)
,
A
B
,
Lemmas
nat
wf
,
not
wf
origin
T:Type. no_repeats(T; []) T:Type. no_repeats(T; []) 
T
A
Qx:A. B(x)
B